NASA R2U2 사이버-물리 시스템을 위한 런타임 검증 프레임워크

NASA R2U2 사이버-물리 시스템을 위한 런타임 검증 프레임워크

2025-11-30, G30DR

1. 서론

1.1 항공우주 시스템의 복잡성과 검증의 난제

현대의 항공우주 및 국방 산업에서 운용되는 시스템은 과거와 비교할 수 없을 정도로 고도화된 복잡성을 띠고 있다. 무인 항공기(UAS), 자율 주행 로버, 위성, 그리고 인간과 협업하는 로봇 시스템(Human-Robot Interaction) 등은 수많은 센서와 액추에이터, 그리고 이를 제어하는 수십만 라인 이상의 임베디드 소프트웨어로 구성된 거대한 사이버-물리 시스템(Cyber-Physical Systems, CPS)이다. 이러한 시스템들은 극한의 환경에서 임무를 수행해야 하며, 사소한 오류가 임무 실패는 물론 막대한 경제적 손실과 인명 피해로 직결될 수 있는 ‘안전 필수(Safety-Critical)’ 시스템으로 분류된다.

전통적으로 이러한 시스템의 신뢰성을 보장하기 위해 설계 단계에서 수행되는 정적 분석(Static Analysis)이나 모델 체킹(Model Checking)과 같은 정형 기법(Formal Methods)들이 활용되어 왔다. 그러나 시스템의 상태 공간(State Space)이 기하급수적으로 증가함에 따라, 설계 단계에서 모든 가능한 시나리오를 완벽하게 검증하는 것은 계산 복잡도 측면에서 한계에 봉착했다. 특히, 외부 환경의 불확실성과 상호작용해야 하는 자율 시스템의 경우, 설계 시점에 예측하지 못한 상황이 런타임(Runtime)에 발생할 확률이 여전히 존재한다. 따라서 시스템이 운용되는 동안 실시간으로 요구사항 준수 여부를 감시하고, 이상 징후를 조기에 포착하여 대응할 수 있는 ‘런타임 검증(Runtime Verification, RV)’ 기술의 중요성이 그 어느 때보다 강조되고 있다.

1.2 런타임 검증(Runtime Verification)의 부상

런타임 검증은 시스템의 실제 실행 추적(Execution Trace)을 관찰하여 사전에 정의된 정형 규격(Formal Specification)을 만족하는지 여부를 실시간으로 판별하는 기술이다. 이는 전체 상태 공간을 탐색해야 하는 모델 체킹과 달리, 현재 실행 중인 경로만을 분석하므로 계산 비용이 상대적으로 낮고 대규모 시스템에도 적용 가능하다는 장점이 있다.

그러나 항공우주 분야에 런타임 검증을 적용하기 위해서는 몇 가지 까다로운 제약 조건을 극복해야 한다. 첫째, 검증 도구가 시스템의 자원(CPU, 메모리, 전력 등)을 과도하게 점유해서는 안 된다. 항공용 임베디드 프로세서는 지상의 워크스테이션에 비해 성능이 현저히 낮기 때문이다. 둘째, 검증 도구 자체가 시스템의 타이밍이나 동작에 영향을 주어서는 안 된다. 이는 엄격한 항공 소프트웨어 인증(예: DO-178C)을 통과하기 위한 필수 조건이다. 셋째, 단순한 오류 탐지를 넘어, 복잡한 시간적 제약 조건(예: “이벤트 A 발생 후 5초 이내에 B가 발생해야 함”)을 처리할 수 있는 강력한 표현력이 요구된다.

1.3 R2U2 프로젝트의 배경 및 목적

NASA 에임스 연구센터(Ames Research Center)와 아이오와 주립대학교(Iowa State University) 등의 연구진이 주도하여 개발한 **R2U2 (Realizable, Responsive, Unobtrusive Unit)**는 앞서 언급한 항공우주 시스템의 제약 사항을 근본적으로 해결하기 위해 고안된 런타임 검증 및 시스템 건강 관리(System Health Management, SHM) 프레임워크이다. R2U2는 이름에서 표방하듯이 실현 가능성(Realizability), 반응성(Responsiveness), **비간섭성(Unobtrusiveness)**이라는 세 가지 핵심 설계 원칙을 바탕으로 개발되었다.

이 프레임워크는 FPGA(Field Programmable Gate Array) 하드웨어와 C/C++/Rust 소프트웨어 등 다양한 플랫폼에서 동작할 수 있도록 유연하게 설계되었으며, 시제 논리(Temporal Logic) 기반의 결정론적 감시와 베이지안 네트워크(Bayesian Networks) 기반의 확률적 진단을 결합하여 강력한 분석 능력을 제공한다. 본 보고서는 R2U2의 아키텍처, 이론적 기반, 구현 기술, 그리고 NASA의 실제 미션 적용 사례를 망라하여 심층적으로 분석한다.

2. R2U2의 핵심 철학: 3대 요구사항

R2U2라는 명칭은 이 도구가 만족해야만 하는, 그리고 항공우주 인증을 위해 필수적인 세 가지 요구사항의 두문자어에서 유래하였다. 이 세 가지 원칙은 R2U2의 모든 설계 결정에 근간이 된다.1

2.1 실현 가능성 (Realizability)

실현 가능성은 R2U2가 이론적인 모델에 그치지 않고, 실제 물리적 제약을 가진 임베디드 시스템 내에서 유의미한 검증을 수행할 수 있어야 함을 의미한다. 이는 크게 **표현력(Expressiveness)**과 **적응성(Adaptability)**의 두 가지 측면으로 나뉜다.

  • 충분한 표현력: 단순한 센서 값의 임계치 초과 여부(Limit Checking)를 확인하는 것만으로는 복잡한 자율 시스템의 안전성을 보장할 수 없다. R2U2는 **Mission-time Linear Temporal Logic (MLTL)**과 같은 고급 시제 논리를 지원하여, 시간의 흐름에 따른 사건의 순서와 지속 시간 등 복합적인 요구사항을 기술할 수 있다. 또한, 불확실한 센서 데이터 하에서 근본 원인을 찾기 위해 베이지안 네트워크를 통합함으로써 논리적 판단과 확률적 추론을 동시에 수행한다. 이러한 다층적 추론 능력은 실제 미션에서 요구되는 고차원적인 건전성 관리(SHM)를 실현 가능하게 한다.
  • 플랫폼 적응성: R2U2는 특정 하드웨어에 종속되지 않는 “플러그 앤 플레이(Plug-and-play)” 아키텍처를 지향한다. 이는 고성능의 지상 관제 시스템부터 자원이 극도로 제한된 초소형 큐브샛(CubeSat)이나 로봇의 관절 제어기 FPGA에 이르기까지, 다양한 타겟 플랫폼에 이식될 수 있음을 의미한다. V3.0에 이르러서는 하드웨어(VHDL)와 소프트웨어(C, C++, Rust) 구현체 간의 사양 파일 호환성을 보장하여, 개발 단계의 시뮬레이션 환경과 실제 비행 환경 간의 매끄러운 전환을 지원한다.

2.2 반응성 (Responsiveness)

안전 필수 시스템에서 위험 상황에 대한 탐지는 즉각적이어야 한다. 반응성은 R2U2가 시스템을 지속적으로 모니터링하고, 실시간으로 추론 결과를 보고하며, 가능한 가장 빠른 시점에 판정(Verdict)을 내려야 함을 규정한다.

  • 실시간 추론 (Real-time Reasoning): R2U2는 입력 데이터 스트림이 들어오는 즉시 처리를 수행하여, 시스템 클록 단위 또는 사전에 보장된 짧은 지연 시간(Latency) 내에 결과를 출력한다. 이는 자율 주행 차량이나 드론이 충돌 직전의 상황과 같이 밀리초(ms) 단위의 대응이 필요한 시나리오에서 필수적이다.
  • 조기 판정 (Early Evaluation): 많은 시제 논리 모니터들은 전체 시계열 데이터가 확보될 때까지 판정을 유보하는 경우가 많다. 그러나 R2U2는 점진적 알고리즘을 사용하여, 미래의 데이터가 없더라도 현재까지의 정보만으로 규격의 위반(Violation)이나 만족(Satisfaction)이 확정되는 즉시 결과를 보고한다. 이를 통해 시스템은 위험 상황 발생 직후 즉각적인 안전 조치(Mitigation)를 취할 수 있다.
  • 중간 상태 보고: 최종 판정뿐만 아니라 매 시간 단계(Time Step)마다 모니터링 상태를 보고함으로써, 지상 관제소나 상위 제어기가 시스템의 건전성 추이를 실시간으로 파악할 수 있도록 돕는다.

2.3 비간섭성 (Unobtrusiveness)

항공우주 소프트웨어 인증 과정에서 가장 까다로운 부분 중 하나는 검증 도구 자체가 시스템의 동작을 변경시키지 않음을 증명하는 것이다. 이를 ’탐침 효과(Probe Effect)’라고 하는데, R2U2는 이를 원천적으로 차단하는 비간섭성을 핵심 가치로 삼는다.

  • 기능적 무결성: R2U2의 동작은 모니터링 대상 시스템(System Under Test, SUT)의 기능적 결과에 어떠한 영향도 주지 않아야 한다. 즉, R2U2가 켜져 있든 꺼져 있든 항공기의 비행 제어 로직은 동일한 입출력 값을 가져야 한다.
  • 타이밍 보존: 소프트웨어 기반 모니터링의 경우, 감시 코드가 CPU 사이클을 소모하여 원래 작업(Task)의 데드라인을 놓치게 만들 수 있다. R2U2는 FPGA 하드웨어 구현을 통해 CPU 오버헤드를 ’0’으로 만들거나, 별도의 코프로세서를 활용하여 타이밍 간섭을 최소화한다.
  • 자원 제약 준수: 크기, 무게, 전력(SWaP) 및 원격 측정(Telemetry) 대역폭이 제한적인 환경에서도 동작할 수 있도록 설계되었다. R2U2는 메모리 사용량을 최소화하고 예측 가능한 수준으로 유지하여, 시스템의 가용 자원을 고갈시키지 않는다. 이는 엄격한 SWaP 제약을 가진 소형 위성이나 드론 미션에서 R2U2가 채택될 수 있었던 결정적인 요인이다.

3. 이론적 배경: 시제 논리 및 정형 명세

R2U2의 강력한 검증 능력은 엄밀한 수학적 논리에 기반을 두고 있다. 특히, 시간의 흐름과 제약 조건을 다루는 시제 논리(Temporal Logic)는 R2U2의 핵심 엔진을 구성한다.3

3.1 선형 시제 논리(LTL)와 한계

선형 시제 논리(Linear Temporal Logic, LTL)는 시스템의 실행 경로를 시간의 흐름에 따른 상태의 순서로 모델링하여 검증하는 데 널리 사용된다. LTL은 Global(\square), Future(\diamond), Next(X), Until(U) 등의 연산자를 사용하여 “언제나 안전해야 한다” 또는 “요청이 있으면 언젠가는 응답해야 한다“와 같은 속성을 기술한다.

그러나 표준 LTL은 무한한 실행 경로(Infinite Traces)를 가정하며, 시간의 개념이 추상적이다. 즉, “언젠가(Eventually)“라는 표현은 실제 임무에서 “5초 이내에“와 같은 구체적인 시간 제한을 표현하기에 부적합하다. 또한, 무한한 시간을 다루는 알고리즘은 유한한 자원을 가진 임베디드 시스템에서 실시간으로 실행하기에 계산 복잡도가 높다.

3.2 Metric Temporal Logic (MTL)

이러한 LTL의 한계를 극복하기 위해 제안된 것이 Metric Temporal Logic (MTL)이다. MTL은 시간 연산자에 실수(Real number) 구간을 적용하여 시간 제약을 명시한다. 예를 들어, \diamond_{} p는 “0초에서 5초 사이의 구간 내에 p가 참이 되어야 한다“는 것을 의미한다. MTL은 시간의 물리적 개념을 도입했지만, 연속 시간(Continuous Time)을 다루는 특성상 디지털 시스템에서의 구현과 검증이 여전히 복잡할 수 있다.

3.3 Mission-time Linear Temporal Logic (MLTL) 상세 분석

R2U2는 항공우주 미션의 특성에 최적화된 **Mission-time Linear Temporal Logic (MLTL)**을 채택하였다. MLTL은 MTL의 변형으로, 유한한 시간(Finite Trace)과 이산적인 정수 시간(Discrete Integer Time) 모델을 기반으로 한다.

3.3.1 문법 및 의미론 (Syntax and Semantics)

MLTL은 시스템 클록이나 샘플링 주기에 매핑되는 정수형 시간 단위를 사용한다. 이는 디지털 제어 시스템의 동작 방식과 정확히 일치하여 런타임 검증에 매우 효율적이다. MLTL의 주요 연산자와 의미는 다음과 같다.5

  • Global (Always, \square_{[lb, ub]}): 현재 시점으로부터 lb (Lower Bound)와 ub (Upper Bound) 사이의 모든 시점에서 조건이 참이어야 한다.

\pi, i \models \square_{[lb, ub]} \phi \iff \forall k \in [i+lb, i+ub], \pi, k \models \phi

  • Future (Eventually, \diamond_{[lb, ub]}): 구간 [lb, ub] 내의 적어도 한 시점에서 조건이 참이어야 한다.

\pi, i \models \diamond_{[lb, ub]} \phi \iff \exists k \in [i+lb, i+ub] \text{ s.t. } \pi, k \models \phi

  • Until (U_{[lb, ub]}): 조건 \phi_1이 지속되다가 구간 [lb, ub] 내에 \phi_2가 참이 되어야 한다.

\pi, i \models \phi_1 U_{[lb, ub]} \phi_2

  • Next (X) 연산자의 배제: R2U2의 MLTL 구현에서는 일반적으로 표준 LTL의 Next 연산자를 사용하지 않거나, D_{} (Delay)로 대체하여 사용한다. 이는 Next 연산자가 샘플링 주기에 지나치게 의존적이며, 시스템 설계 변경 시 규격을 재작성해야 하는 문제를 야기할 수 있기 때문이다. 대신 구간 기반 연산자를 사용하여 보다 견고한(Robust) 명세를 작성하도록 유도한다.

3.3.2 3치 논리(Three-valued Logic)와 가정-보장 계약

R2U2 V3.0에서는 복잡한 시스템의 구성 요소 간 인터페이스를 명확히 정의하기 위해 가정-보장 계약(Assume-Guarantee Contracts, AGC) 패턴을 지원한다. 이를 효과적으로 처리하기 위해, R2U2는 전통적인 True/False 외에 Inactive라는 세 번째 상태를 도입한 3치 논리를 사용한다.4

  • True: 가정이 만족되고 보장 조건도 만족된 경우.
  • False: 가정이 만족되었으나 보장 조건이 위배된 경우 (규격 위반).
  • Inactive: 가정 조건 자체가 만족되지 않은 경우. 이 경우 해당 규격은 현재 상황에 적용되지 않으므로 ’거짓’이 아닌 ‘비활성’ 상태로 처리하여 오탐을 방지한다.

이러한 논리적 확장은 미션 단계(Phase)에 따라 서로 다른 요구사항이 적용되는 항공우주 시스템의 특성을 정확하게 반영할 수 있게 해준다.

4. R2U2 시스템 아키텍처

R2U2 아키텍처는 유연성을 극대화하기 위해 모듈화되어 있으며, 크게 하드웨어(FPGA) 버전과 소프트웨어 버전으로 나뉜다. 두 버전 모두 논리적 처리 흐름은 동일하지만, 데이터 수집 및 처리 방식에서 플랫폼별 최적화가 이루어져 있다.7

4.1 하드웨어 기반 구현 (FPGA)

FPGA 구현은 R2U2가 “비간섭성“을 달성하는 가장 강력한 수단이다. 주로 Xilinx Zynq와 같은 SoC(System on Chip)나 별도의 FPGA 칩에 IP(Intellectual Property) 코어 형태로 탑재된다.

4.1.1 IP 코어 설계 및 통합

R2U2 하드웨어 모듈은 VHDL로 작성된 커스텀 IP 코어이다. 이 코어는 타겟 시스템의 메인 프로세서와 독립적으로 동작하는 별도의 회로로 구성된다.

  • 자원 효율성: Xilinx Zynq XC7Z010과 같은 저가형 FPGA에서도 슬라이스 레지스터의 약 40%, LUT(Look-Up Table)의 64%만을 사용하여 전체 시스템을 구현할 수 있다.8 이는 남은 FPGA 공간을 비행 제어 등 다른 목적에 사용할 수 있게 해주거나, 매우 작은 FPGA에도 R2U2를 탑재할 수 있음을 의미한다.
  • 소프트 IP vs 하드 IP: R2U2는 FPGA의 범용 로직(LUT, Flip-flop)을 사용하여 구성되는 ’소프트 IP’의 성격을 띠지만, 성능 최적화를 위해 FPGA 내장 DSP 블록 등을 활용하기도 한다.

4.1.2 버스 스니핑 및 메모리 접근

하드웨어 R2U2는 ’수동적 감시자(Passive Observer)’로서 동작한다.

  • 버스 모니터링: 시스템 버스(AMBA AXI, SPI, I2C 등)에 연결되어, CPU와 주변장치 간에 오가는 데이터를 ’도청(Sniffing)’한다. 이 과정은 전기적으로 신호를 읽기만 할 뿐 버스 트래픽을 유발하거나 CPU의 실행 흐름을 방해하지 않는다.
  • 격리성(Isolation): R2U2 하드웨어는 물리적으로 분리된 메모리와 로직을 가지므로, 메인 소프트웨어가 버그로 인해 멈추거나 해킹을 당하더라도 R2U2는 계속해서 살아서 감시를 수행할 수 있다. 이는 보안 위협 탐지에 있어 결정적인 장점이다.

4.2 소프트웨어 기반 구현

FPGA가 없는 시스템이나, 더 높은 수준의 소프트웨어 통합이 필요한 경우를 위해 C, C++, Rust 버전이 제공된다.

4.2.1 cFS (core Flight System) 통합

NASA의 표준 비행 소프트웨어 프레임워크인 **cFS(core Flight System)**와의 통합은 R2U2의 범용성을 보여주는 대표적인 예이다.2

  • R2U2는 cFS의 ‘애플리케이션(App)’ 형태로 통합되어, 소프트웨어 버스(Software Bus)를 통해 발행되는 메시지(Telemetry)를 구독(Subscribe)한다.
  • 이 방식은 기존 비행 소프트웨어 코드를 수정(Instrumentation)할 필요 없이, 메시지 인터페이스만을 통해 데이터를 수집하므로 비간섭성을 어느 정도 유지할 수 있다.

4.2.2 C, C++, Rust 구현체 비교

  • C/C++: 가장 널리 사용되는 버전으로, 임베디드 리눅스나 베어메탈(Bare-metal) 환경에서 높은 이식성을 가진다. 자원 사용량이 적고 속도가 빠르다.
  • Rust: 최신 R2U2 V3.0 개발 흐름에서는 Rust 언어를 도입하고 있다.9 Rust는 컴파일 타임에 메모리 안전성을 보장하므로, 검증 도구 자체의 버그로 인한 시스템 충돌 가능성을 더욱 낮춰준다. 이는 안전 필수 시스템의 트렌드와 부합한다.

4.3 병렬 처리 아키텍처 (Epiphany Coprocessor)

고성능이 요구되는 경우, 다중 코어 프로세서를 활용한 병렬 처리가 적용된다.

  • Epiphany 아키텍처: Adapteva Parallella 보드에 탑재된 16코어 또는 64코어 Epiphany 코프로세서 상에서 R2U2/E 버전을 구동한 연구가 있다.10
  • MIMD 병렬화: 각 코어에 서로 다른 시제 논리 관찰자를 할당하여(MIMD: Multiple Instruction, Multiple Data), 수백 개의 복잡한 규격을 동시에 병렬로 검사한다.
  • 공유 메모리: 호스트 CPU와 코프로세서 간에 DMA(Direct Memory Access) 기반 공유 메모리를 사용하여 데이터 전송 오버헤드를 최소화한다.

5. 추론 엔진의 내부 구성

R2U2의 추론 엔진은 원시 데이터를 의미 있는 정보로 변환하고, 이를 바탕으로 논리적, 확률적 판단을 내리는 3단계 파이프라인으로 구성된다.

5.1 신호 전처리 및 원자 검사기 (Atomic Checkers)

시스템 버스나 센서로부터 들어오는 데이터는 int, float 등의 수치 데이터이다. 논리 엔진이 이를 처리하기 위해서는 True/False의 불리언(Boolean) 값으로 변환해야 한다. 이를 담당하는 것이 **원자 검사기(Atomic Checkers)**이다.11

  • 기능: 단순한 비교 연산(예: 속도 > 100)뿐만 아니라, 필터링 기능을 내장하고 있다.
  • 확장 모드: 노이즈가 많은 센서 데이터를 처리하기 위해 이동 평균(Moving Average), 변화율(Rate), 절대 차이(Absolute Difference) 등의 전처리 함수를 적용한 후 임계치를 비교한다.4 예를 들어, abs_diff_angle(s3, 105) < 50과 같은 표현을 통해 센서 값의 변동폭을 검사할 수 있다. 이는 오탐(False Alarm)을 줄이는 데 핵심적인 역할을 한다.

5.2 시제 논리 관찰자 (Temporal Observers)

전처리된 불리언 신호는 시제 논리 관찰자로 전달되어 시간적 패턴을 검사한다.

5.2.1 AST 기반 실행 모델

초기의 런타임 검증 도구들은 주로 오토마타(Automata) 변환 방식을 사용했으나, R2U2는 추상 구문 트리(Abstract Syntax Tree, AST) 기반의 접근 방식을 채택했다.4

  • 오토마타 방식은 복잡한 수식에 대해 상태 공간 폭발을 일으킬 수 있는 반면, AST 방식은 수식의 구조를 그대로 트리로 매핑하여 순회(Traversal)하는 방식이므로 메모리 사용량이 수식의 길이에 선형적으로 비례한다. 이는 자원이 제한된 시스템에서 예측 가능한 메모리 사용량을 보장한다.

5.2.2 효율적인 인코딩 전략

R2U2는 C2PO 컴파일러를 통해 MLTL 수식을 최적화된 어셈블리 형태의 명령어 세트로 변환한다. 이 명령어들은 런타임 엔진에 의해 해석(Interpret)되거나 FPGA 로직으로 합성된다. 비동기적(Asynchronous) 관찰자 설계를 통해, 미래의 값이 도착하지 않아도 현재 값만으로 결과가 확정되면 즉시 판정을 내리는 효율성을 갖추고 있다.12

5.3 베이지안 네트워크 추론기 (Bayesian Network Reasoners)

시제 논리가 “규격이 위반되었는가?”(예/아니오)를 판단한다면, 베이지안 네트워크는 “그 원인은 무엇이며, 시스템의 현재 건강 상태는 어떠한가?”(확률)를 추론한다.2

5.3.1 산술 회로 변환

베이지안 네트워크의 추론은 일반적으로 NP-Hard 문제에 속할 만큼 계산 비용이 높다. R2U2는 실시간성을 보장하기 위해, 베이지안 네트워크를 **산술 회로(Arithmetic Circuit, AC)**로 컴파일하여 사용한다. AC는 덧셈과 곱셈 연산만으로 구성된 회로 구조로, FPGA나 임베디드 프로세서에서 매우 빠르게 확률 값을 계산할 수 있다.

5.3.2 확률적 건전성 진단

시제 논리 관찰자의 출력(규격 위반 여부)이 베이지안 네트워크의 증거(Evidence) 노드로 입력된다. 추론기는 이를 바탕으로 센서 고장, 액추에이터 고장, 또는 보안 공격 등의 사후 확률(Posterior Probability)을 계산한다. 예를 들어, GPS 신호와 관성항법장치(IMU) 신호가 불일치한다는 시제 논리 결과가 나오면, 베이지안 네트워크는 이것이 GPS 스푸핑 공격일 확률이 95%, 단순 센서 고장일 확률이 5%라는 식의 진단을 내릴 수 있다.

6. 개발 툴체인 및 워크플로우 (Version 3.0)

R2U2 V3.0은 사용자 편의성과 생산성을 높이기 위해 **C2PO (Configuration Compiler for Property Organization)**라는 강력한 툴체인을 도입했다.4

6.1 C2PO (Configuration Compiler for Property Organization)

C2PO는 사용자가 작성한 고수준의 명세를 R2U2 엔진이 이해할 수 있는 저수준의 바이너리 설정 파일이나 VHDL/C 코드로 변환해주는 컴파일러이다. Python으로 개발되었으며, 복잡한 수식을 최적화하는 기능을 수행한다.

6.2 명세 언어 및 최적화

  • 고수준 언어: C2PO는 C언어와 유사한 문법을 지원한다. 구조체(Struct)를 정의하여 관련 신호들을 묶을 수 있고, 매크로와 함수를 사용하여 반복되는 수식을 모듈화할 수 있다.
  • 집합 연산(Set Aggregation): foreach 구문이나 집합 연산을 지원하여, 수십 개의 센서에 대해 동일한 규칙을 적용해야 할 때 코드를 간결하게 작성할 수 있다.4 예를 들어, “모든 온도 센서의 값이 100도 미만이어야 한다“는 규칙을 단 한 줄로 표현할 수 있다.
  • 최적화: 컴파일 과정에서 공통 하위 식 제거(Common Subexpression Elimination) 등의 최적화를 수행하여, 생성되는 관찰자의 크기와 실행 시간을 최소화한다.

6.3 리소스 예측 및 시각화 도구

C2PO는 컴파일 단계에서 해당 명세가 타겟 FPGA에서 얼마나 많은 리소스(LUT, 레지스터)를 사용할지, 또는 소프트웨어 엔진에서 최악의 경우 실행 시간(WCET)이 얼마나 걸릴지를 미리 예측하여 보고한다.4 또한, 웹 기반의 GUI 도구를 통해 AST 구조를 시각화하고 디버깅할 수 있는 환경을 제공하여 개발자가 명세의 논리적 오류를 쉽게 찾을 수 있도록 돕는다.14

7. 주요 적용 사례 연구 (Case Studies)

R2U2는 단순한 연구용 프로토타입을 넘어 NASA의 실제 미션 및 다양한 항공우주 시스템에서 그 효용성을 입증해 왔다.

7.1 NASA Robonaut 2 (R2) 무릎 관절 고장 진단

국제우주정거장(ISS)에서 우주비행사를 보조하는 휴머노이드 로봇 Robonaut 2 (R2)는 무릎 관절 제어기에서 간헐적인 이상 동작을 보였다.11

  • 도전 과제: 지상에서 원격으로 디버깅하기에는 대역폭이 부족했고, 기존 제어 소프트웨어를 수정하면 안전 인증을 다시 받아야 하는 문제가 있었다. 또한, FPGA의 여유 공간이 매우 부족했다.
  • R2U2 적용: R2U2를 관절 제어기 FPGA의 남은 공간(Left-over space)에 탑재하였다. R2U2는 관절의 위치 센서(Encoder) 값과 제어 명령을 모니터링하면서, 센서의 일시적인 노이즈인지 실제 하드웨어 고장인지를 구분하는 MLTL 규격을 실시간으로 검사했다.
  • 결과: R2U2는 기존 제어 루프에 전혀 영향을 주지 않으면서(Unobtrusive), 고장 상황을 정확히 식별(Disambiguation)해냈다. 이를 통해 잘못된 센서 데이터로 인한 로봇의 오동작을 방지하고 안전 모드(Safe Mode)로의 전환을 트리거할 수 있었다.

7.2 NASA Lunar Gateway: Vehicle System Manager (VSM)

유인 달 탐사 정거장인 루나 게이트웨이(Lunar Gateway)는 사람의 개입 없이 장기간 자율 운용되어야 한다. 이를 관리하는 핵심 소프트웨어가 **Vehicle System Manager (VSM)**이다.3

  • 도전 과제: VSM은 복잡한 자율 의사결정을 수행하므로, 모든 상태를 사전에 검증하기 어렵다.
  • R2U2 적용: NASA는 광범위한 조사 끝에 VSM의 런타임 검증 도구로 R2U2를 선정했다. cFS 환경 내에서 동작하며, 가정-보장 계약(Assume-Guarantee Contracts)을 기반으로 작성된 MLTL 명세를 통해 VSM의 건전성을 실시간으로 감시한다. 이는 R2U2가 차세대 우주 정거장의 안전을 책임지는 핵심 기술로 인정받았음을 시사한다.

7.3 무인 항공기(UAS): DragonEye 및 Swift 보안 모니터링

NASA의 소형 무인기 DragonEye와 Swift를 대상으로 한 실험에서는 R2U2의 보안 위협 탐지 능력이 검증되었다.8

  • 시나리오: GPS 스푸핑 공격이나 지상 관제소 탈취 시나리오가 시뮬레이션되었다.
  • R2U2 적용: 시제 논리 관찰자는 비행 궤적이 물리적으로 불가능한 패턴(예: 순간적인 위치 이동)을 보이는지 감시하고, 베이지안 네트워크는 이것이 센서 고장인지 악의적인 공격인지 확률적으로 판단했다.
  • 결과: 공격 발생 시 실시간으로 위협을 탐지하고 조종사에게 경고를 보낼 수 있음을 입증했다. 하드웨어 기반의 독립적인 모니터링 덕분에 비행 컴퓨터가 악성코드에 감염되더라도 R2U2는 안전하게 위협을 알릴 수 있었다.

7.4 소형 위성 및 로켓: CySat-I, Nova Somnium

R2U2는 자원이 극도로 제한된 큐브샛(CubeSat)과 사운딩 로켓(Sounding Rocket)에도 적용되었다.14

  • Nova Somnium: 아이오와 주립대의 사운딩 로켓 프로젝트에서 R2U2는 발사체의 비행 상태를 실시간으로 감시하고, 낙하산 전개 시점 등의 임무 중요 이벤트가 규격대로 발생하는지 검증했다.
  • CySat-I: 큐브샛의 경우 전력과 처리 능력이 매우 부족하지만, R2U2의 효율적인 아키텍처 덕분에 탑재가 가능했다. 위성의 자세 제어 시스템(ADCS)과 통신 시스템의 건전성을 궤도상에서 모니터링하는 역할을 수행했다.

7.5 AI/ML 시스템 모니터링: SYSAI 통합

최근에는 인공지능(AI) 및 머신러닝(ML) 구성 요소를 포함한 시스템의 안전성 확보를 위해 R2U2가 활용되고 있다.17

  • 문제: 신경망(Neural Network)은 내부 동작을 예측하기 어려운 ‘블랙박스’ 특성을 가지며, 정형 검증이 매우 어렵다.
  • 해결: SYSAI (System Analysis using Statistical AI) 프레임워크와 R2U2를 결합하여, 런타임에 신경망의 입출력 패턴을 통계적으로 분석하고 안전 규격을 위반하는지 감시한다. 예를 들어, 자율 주행 신경망이 차선을 이탈하는 제어 명령을 내릴 때, R2U2가 이를 감지하고 안전 제어기로 권한을 넘기는(Fail-over) 구조를 구현할 수 있다.

8. 성능 분석 및 자원 효율성

8.1 FPGA 리소스 점유율 분석

R2U2의 하드웨어 효율성은 정량적인 수치로 입증된다. 다음 표는 Xilinx Zynq XC7Z010 FPGA에서의 R2U2 구현 시 리소스 사용량을 보여준다.8

리소스 유형사용량 비율비고
Slice Registers~40%MLTL 수식의 복잡도와 무관하게 일정 수준 유지
Slice LUTs~64%128개의 입력 신호를 처리하는 구성 기준
DSP Blocks가변적산술 연산 최적화 시 사용

이 데이터는 R2U2가 저사양 FPGA의 절반 정도의 리소스만으로도 강력한 모니터링 기능을 수행할 수 있음을 보여준다.

8.2 오버헤드 및 지연 시간(Latency) 평가

  • 오버헤드: FPGA 구현 시 메인 CPU에 대한 오버헤드는 ’0’이다. 소프트웨어 구현 시에도 최적화된 AST 순회를 통해 매우 낮은 CPU 점유율을 보인다.
  • 지연 시간: 하드웨어 R2U2는 입력 신호 변화 후 단일 클록 사이클 내에, 혹은 결정론적인 수 클록 사이클 내에 판정 결과를 출력한다. 이는 kHz 단위의 제어 루프를 가진 고속 시스템에서도 충분히 실시간성을 보장할 수 있는 수준이다.18

8.3 경쟁 도구 비교 분석

도구명플랫폼주요 특징한계점R2U2의 우위
R2U2HW/SW3대 원칙(Realizable, Responsive, Unobtrusive), MLTL+Bayesian초기 학습 곡선 존재하드웨어 격리, 진단 기능 통합, 항공 인증 고려 설계
BusMOPHW버스 모니터링, 오버헤드 0임의 코드 실행 가능R2U2는 정형 명세만 허용하여 인증 용이성 및 예측 가능성 확보 8
CopilotSW하드 리얼타임 C 코드 생성SW 전용FPGA를 통한 물리적 격리 및 무오버헤드 구현 불가 6
LolaSW스트림 기반 모니터링효율적인 스트림 처리베이지안 진단 기능의 부재

9. 결론 및 향후 전망

NASA R2U2 프레임워크는 항공우주 및 사이버-물리 시스템의 안전성을 보장하기 위한 런타임 검증 기술의 정점을 보여준다. “실현 가능성”, “반응성”, “비간섭성“이라는 세 가지 철학을 바탕으로, 이론적인 시제 논리를 척박한 임베디드 환경에 성공적으로 안착시켰다.

R2U2의 핵심 기여는 다음과 같이 요약할 수 있다.

  1. 정형 기법의 민주화: 난해한 수학적 이론을 C2PO와 같은 툴체인을 통해 현장의 엔지니어가 접근 가능한 기술로 변환하였다.
  2. 하드웨어 레벨의 최후 방어선 구축: FPGA를 활용한 독립적인 감시 아키텍처는 소프트웨어 오류나 사이버 공격으로부터 시스템을 보호하는 강력한 안전장치를 제공한다.
  3. 진단과 검증의 통합: 단순한 규격 위반 탐지를 넘어, 베이지안 추론을 통한 원인 분석까지 제공함으로써 자율 시스템의 상황 인식 능력을 획기적으로 향상시켰다.

향후 R2U2는 Rust 언어 지원 강화를 통해 소프트웨어 안정성을 더욱 높이고, AI/ML 시스템에 대한 검증 기능을 확대하여 완전 자율 주행 시대를 대비하는 핵심 안전 기술로 진화할 것이다. 루나 게이트웨이와 같은 인류의 거대한 도전 과제 속에서, R2U2는 보이지 않는 곳에서 시스템의 안녕을 지키는 든든한 파수꾼 역할을 수행하고 있다. 이는 안전 필수 시스템을 다루는 모든 엔지니어와 연구자들이 주목해야 할 기술적 이정표이다.

참고 자료

  1. R2U2: Tool Overview - NASA Technical Reports Server (NTRS), 11월 30, 2025에 액세스, https://ntrs.nasa.gov/citations/20190026747
  2. R2U2: Tool Overview, 11월 30, 2025에 액세스, https://research.temporallogic.org/papers/RS2017_RV.pdf
  3. Procedia Computer Science WEST: Interactive Validation of Mission-time Linear Temporal Logic (MLTL), 11월 30, 2025에 액세스, https://research.temporallogic.org/papers/WGR25.pdf
  4. R2U2 Version 3.0: Re-imagining a Toolchain for Specification, Resource Estimation, and Optimized Observer Generation for Runtime Verification in Hardware and Software - Chris Johannsen, 11월 30, 2025에 액세스, https://cgjohannsen.com/papers/JJKRZ23.pdf
  5. Maximum Satisfiability of Mission-time Linear Temporal Logic - Tichakorn (Nok) Wongpiromsarn, 11월 30, 2025에 액세스, https://tichakorn.dev/publication/hariharan-2023-maximum/hariharan-2023-maximum.pdf
  6. Integrating Runtime Verification into an Automated UAS Traffic Management System - R2U2, 11월 30, 2025에 액세스, https://r2u2.temporallogic.org/wp-content/uploads/2020/12/CHHJR20.pdf
  7. Software and System Health Management with R2U2, 11월 30, 2025에 액세스, https://ntrs.nasa.gov/api/citations/20190033108/downloads/20190033108.pdf
  8. R2U2: Monitoring and Diagnosis of Security Threats for Unmanned Aerial Systems - NASA Technical Reports Server (NTRS), 11월 30, 2025에 액세스, https://ntrs.nasa.gov/citations/20150023544
  9. Overview — R2U2 Documentation, 11월 30, 2025에 액세스, https://r2u2.github.io/r2u2/
  10. Unobtrusive Software and System Health Management with R2U2 on a parallel MIMD Coprocessor, 11월 30, 2025에 액세스, https://ntrs.nasa.gov/api/citations/20170011649/downloads/20170011649.pdf
  11. Embedding Online Runtime Verification for Fault Disambiguation on Robonaut2 - Iowa State University, 11월 30, 2025에 액세스, https://www.ece.iastate.edu/~zambreno/assets/pdf/KemZha20A.pdf
  12. Embedding Online Runtime Verification for Fault Disambiguation on …, 11월 30, 2025에 액세스, https://temporallogic.org/research/FORMATS20/r2-r2u2.pdf
  13. R2U2 V3.0 - Re-imagining a Toolchain for Specification, Resource Estimation, and Optimized Observer Generation for Runtime Verif - Chris Johannsen, 11월 30, 2025에 액세스, https://cgjohannsen.com/slides/JJKRZ23.pdf
  14. R2U2 Playground: Visualization of a Real-time, Temporal Logic Runtime Monitor - reposiTUm, 11월 30, 2025에 액세스, https://repositum.tuwien.at/bitstream/20.500.12708/219547/1/Aurandt-2025-R2U2%20Playground%20Visualization%20of%20a%20Real-time%2C%20Temporal%20Logic…-vor.pdf
  15. R2U2 observers, encoded on the FPGA, monitor internal sensor values passed over the R2 control bus. - ResearchGate, 11월 30, 2025에 액세스, https://www.researchgate.net/figure/R2U2-observers-encoded-on-the-FPGA-monitor-internal-sensor-values-passed-over-the-R2_fig4_343845198
  16. Trusted Autonomous Systems, 11월 30, 2025에 액세스, https://ntrs.nasa.gov/api/citations/20230003721/downloads/TrustedAutonomy_Final.pptx.pdf
  17. Runtime Monitoring for Unmanned Aerospace Systems with Neural Network Components - NASA Technical Reports Server (NTRS), 11월 30, 2025에 액세스, https://ntrs.nasa.gov/citations/20220012988
  18. A Latency-Insensitive Design Approach to Programmable FPGA-Based Real-Time Simulators - MDPI, 11월 30, 2025에 액세스, https://www.mdpi.com/2079-9292/9/11/1838